Nuprl Lemma : member_tl
4,23
postcript
pdf
T
:Type,
as
:
T
List,
x
:
T
. 0<||
as
||
(
x
tl(
as
))
(
x
as
)
latex
Definitions
A
&
B
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
Prop
,
tl(
l
)
,
P
Q
,
A
B
,
P
&
Q
,
i
j
<
k
,
{
i
..
j
}
,
,
P
Q
,
P
Q
,
l
[
i
]
,
i
j
,
False
,
A
Lemmas
length
tl
,
select
wf
,
select
tl
,
le
wf
,
l
member
wf
,
tl
wf
,
length
wf1
origin
T:Type, as:T List, x:T. 0<||as|| 
(x 
tl(as)) (x as) T:Type, as:T List, x:T. 0<||as|| (x tl(as)) (x as) 
x:A. B(x) l) Tx:A. B(x) Q
B j < k
}
Q Q
j
A